\begin{tabbing}
sys{-}order(${\it es}$; ${\it Sys}$; $f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$a_{1}$:es{-}E{-}interface(${\it es}$;${\it Sys}$), $b_{1}$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex]fun{-}connected(es{-}E{-}interface(${\it es}$;${\it Sys}$);$f$;$b_{1}$;$a_{1}$)
\\[0ex]$\Rightarrow$ \=($\forall$$a_{2}$:es{-}E{-}interface(${\it es}$;${\it Sys}$), $b_{2}$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex]fun{-}connected(es{-}E{-}interface(${\it es}$;${\it Sys}$);$f$;$b_{2}$;$a_{2}$)
\\[0ex]$\Rightarrow$ es{-}locl(${\it es}$; $a_{1}$; $a_{2}$)
\\[0ex]$\Rightarrow$ ($\neg$fun{-}connected(es{-}E{-}interface(${\it es}$;${\it Sys}$);$f$;$a_{2}$;$a_{1}$))
\\[0ex]$\Rightarrow$ (es{-}loc(${\it es}$; $b_{1}$) = es{-}loc(${\it es}$; $b_{2}$) $\in$ Id)
\\[0ex]$\Rightarrow$ es{-}locl(${\it es}$; $b_{1}$; $b_{2}$))
\-\-
\end{tabbing}